#include "aig.h"

/**
@brief modified from hash32shift 

http://www.concentric.net/~ttwang/tech/inthash.htm
*/
uint64_t hash64shift(uint64_t a)
{
   a = (a+0x7ed55d16) + (a<<12);
   a = (a^0xc761c23c) ^ (a>>19);
   a = (a+0x165667b1) + (a<<5);
   a = (a+0xd3a2646c) ^ (a<<9);
   a = (a+0xfd7046c5) + (a<<3);
   a = (a^0xb55a4f09) ^ (a>>16);
   return a;
}
AigLit StrashAIG::pseudo_createAND( AigLit a , AigLit b )
{
   if( a > b ){a^=b;b^=a;a^=b;}
   AigNode n( a , b );
   {
      AigHash::iterator iter= _hash.find( n );
      if( iter != _hash.end() ){ return toAigLit( iter->second,0);}
   }
   if( ((~a)|(b)|1) == 0xFFFFFFFF )
   {
      if( a == 0 || (a^b) == 1 ){ return 0 ; }
      if( a == 1 || (a^b) == 0 ){ return b ; }
   }

   unsigned s = sz;
   push( n );

   return toAigLit( s , 0 );
}
AigLit StrashAIG::test_createAND( AigLit a , AigLit b )const
{
   if( a > b ){a^=b;b^=a;a^=b;}
   AigNode n( a , b );
   {
      AigHash::const_iterator iter= _hash.find( n );
      if( iter != _hash.end() ){ return toAigLit( iter->second,0);}
   }
   if( ((~a)|(b)|1) == 0xFFFFFFFF )
   {
      if( a == 0 || (a^b) == 1 ){ return 0 ; }
      if( a == 1 || (a^b) == 0 ){ return b ; }
   }

   return toAigLit( sz , 0 );
}
AigLit StrashAIG::createAND( AigLit a , AigLit b )
{
   if( a > b ){a^=b;b^=a;a^=b;}
   AigNode n( a , b );
   {
      AigHash::iterator iter= _hash.find( n );
      if( iter != _hash.end() ){ return toAigLit( iter->second,0);}
   }
   if( ((~a)|(b)|1) == 0xFFFFFFFF )
   {
      if( a == 0 || (a^b) == 1 ){ return 0 ; }
      if( a == 1 || (a^b) == 0 ){ return b ; }
   }

   unsigned s = size();
   push( n );
   _hash.insert( AigHash::value_type(n,s) );

   return toAigLit( s , 0 );
}
StrashAIG::StrashAIG()
{
   AigNode n; 
   n.key=0;
   _hash.set_empty_key(n);
   n.key=-1;
   _hash.set_deleted_key(n);
   createBase(); 
}
bool StrashAIG::check()const
{
   if( size() - _andFlag != _hash.size() )return false; 
   for( unsigned i = _andFlag ; i < size() ; ++ i )
      if( _hash.find( (*this)[i] ) == _hash.end() )return false;
   if( _ppiFlag > _andFlag       )return false;

   return true;
}

